r:Rng, b:. (when b. 0) = 0  |r| 

latex

Definitions	x:A. B(x), IMonoid, t  T, |g|, e, r+gp, AbGrp, Group{i}, Mon, P & Q, Prop, 1of(t), 2of(t), when b. p
Lemmas	mon when of id, add grp of rng wf b, monoid p wf, grp car wf, grp op wf, grp id wf, abgrp wf, rng wf